Addendum to “Service Automata” – formal proofs –

This document contains the formal proof for Theorem 1 in the article “Service Automata ” [1] (Section 2) and preliminaries for the formalism (Section 1). 1 Preliminaries In the proof, we denote the length of a sequence s by |s|, and the projection of a sequence s to an alphabet E of events by s E. As a shorthand, we write e1, e2 C t for e1 C t and e2 C t. 1.1 A Primer to Hoare’s Communicating Sequential Processes We briefly recall the sublanguage of Hoare’s Communicating Sequential Processes (CSP) used in this article. For a proper introduction, we refer to [2]. A process P is a pair (α(P), traces(P)) consisting of a set of events and a nonempty, prefix-closed set of finite sequences over α(P). The alphabet α(P) contains all events in which P could in principle engage. The set of possible traces traces(P) ⊆ (α(P)) ∗ contains all sequences of events that the process could in principle perform. We use 〈 〉 to denote the empty sequence, 〈e 〉 to denote the trace consisting of the single event e, and s.t to denote the concatenation of two traces s and t. That an event e occurs in a trace t is denoted by e C t. The CSP process expression STOPE specifies a process with alphabet E and a set of trace